0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 183 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 441 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 PiDPToQDPProof (⇒, 36 ms)
↳30 QDP
↳31 QDPOrderProof (⇔, 587 ms)
↳32 QDP
↳33 DependencyGraphProof (⇔, 0 ms)
↳34 QDP
↳35 UsableRulesProof (⇔, 0 ms)
↳36 QDP
↳37 QReductionProof (⇔, 0 ms)
↳38 QDP
↳39 UsableRulesReductionPairsProof (⇔, 12 ms)
↳40 QDP
↳41 PisEmptyProof (⇔, 0 ms)
↳42 YES
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → U6_G(X1, X2, X3, pA_in_g(cons(X1, cons(X2, X3))))
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → PA_IN_G(cons(X1, cons(X2, X3)))
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → U7_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
U7_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U8_G(X1, X2, X3, multB_in_gga(X1, X2, X4))
U7_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → MULTB_IN_GGA(X1, X2, X4)
MULTB_IN_GGA(X1, s(X2), X3) → U1_GGA(X1, X2, X3, multB_in_gga(X1, X2, X4))
MULTB_IN_GGA(X1, s(X2), X3) → MULTB_IN_GGA(X1, X2, X4)
MULTB_IN_GGA(X1, s(X2), X3) → U2_GGA(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U2_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U3_GGA(X1, X2, X3, sumD_in_gga(X4, X1, X3))
U2_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → SUMD_IN_GGA(X4, X1, X3)
SUMD_IN_GGA(X1, s(X2), s(X3)) → U4_GGA(X1, X2, X3, sumD_in_gga(X1, X2, X3))
SUMD_IN_GGA(X1, s(X2), s(X3)) → SUMD_IN_GGA(X1, X2, X3)
U7_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U9_G(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U10_G(X1, X2, X3, pA_in_g(cons(X4, X3)))
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → U15_G(X1, X2, pA_in_g(cons(X1, X2)))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → PA_IN_G(cons(X1, X2))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → U16_G(X1, X2, pcA_in_g(cons(X1, X2)))
U16_G(X1, X2, pcA_out_g(cons(X1, X2))) → U17_G(X1, X2, multC_in_ga(X1, X3))
U16_G(X1, X2, pcA_out_g(cons(X1, X2))) → MULTC_IN_GA(X1, X3)
MULTC_IN_GA(s(X1), X2) → U5_GA(X1, X2, multC_in_ga(X1, X3))
MULTC_IN_GA(s(X1), X2) → MULTC_IN_GA(X1, X3)
U16_G(X1, X2, pcA_out_g(cons(X1, X2))) → U18_G(X1, X2, multcC_in_ga(X1, X3))
U18_G(X1, X2, multcC_out_ga(X1, X3)) → U19_G(X1, X2, pA_in_g(cons(X3, X2)))
U18_G(X1, X2, multcC_out_ga(X1, X3)) → PA_IN_G(cons(X3, X2))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U20_G(X1, X2, X3, pA_in_g(cons(X1, cons(X2, X3))))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → PA_IN_G(cons(X1, cons(X2, X3)))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U21_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
U21_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U22_G(X1, X2, X3, multB_in_gga(X1, X2, X4))
U21_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → MULTB_IN_GGA(X1, X2, X4)
U21_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U23_G(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U23_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U24_G(X1, X2, X3, pA_in_g(cons(X4, X3)))
U23_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
PA_IN_G(cons(0, cons(0, X1))) → U25_G(X1, pA_in_g(X1))
PA_IN_G(cons(0, cons(0, X1))) → PA_IN_G(X1)
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U11_G(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U11_G(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U12_G(X1, X2, X3, multB_in_gga(s(s(X1)), X2, X5))
U11_G(X1, X2, X3, pcA_out_g(cons(X4, X3))) → MULTB_IN_GGA(s(s(X1)), X2, X5)
U11_G(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U13_G(X1, X2, X3, multcB_in_gga(s(s(X1)), X2, X5))
U13_G(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U14_G(X1, X2, X3, pA_in_g(cons(X5, X3)))
U13_G(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → PA_IN_G(cons(X5, X3))
pcA_in_g(cons(X1, nil)) → pcA_out_g(cons(X1, nil))
pcA_in_g(cons(s(s(s(s(X1)))), cons(X2, X3))) → U27_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(s(s(0)), cons(X1, X2))) → U32_g(X1, X2, pcA_in_g(cons(X1, X2)))
pcA_in_g(cons(0, cons(X1, nil))) → pcA_out_g(cons(0, cons(X1, nil)))
pcA_in_g(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U35_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(0, cons(0, X1))) → U38_g(X1, pcA_in_g(X1))
U38_g(X1, pcA_out_g(X1)) → pcA_out_g(cons(0, cons(0, X1)))
U35_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U36_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U39_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U39_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U40_gga(X1, X2, X3, sumcD_in_gga(X4, X1, X3))
sumcD_in_gga(X1, 0, X1) → sumcD_out_gga(X1, 0, X1)
sumcD_in_gga(X1, s(X2), s(X3)) → U41_gga(X1, X2, X3, sumcD_in_gga(X1, X2, X3))
U41_gga(X1, X2, X3, sumcD_out_gga(X1, X2, X3)) → sumcD_out_gga(X1, s(X2), s(X3))
U40_gga(X1, X2, X3, sumcD_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)
U36_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U37_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U37_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → pcA_out_g(cons(0, cons(s(s(X1)), cons(X2, X3))))
U32_g(X1, X2, pcA_out_g(cons(X1, X2))) → U33_g(X1, X2, multcC_in_ga(X1, X3))
multcC_in_ga(0, 0) → multcC_out_ga(0, 0)
multcC_in_ga(s(X1), X2) → U42_ga(X1, X2, multcC_in_ga(X1, X2))
U42_ga(X1, X2, multcC_out_ga(X1, X2)) → multcC_out_ga(s(X1), X2)
U33_g(X1, X2, multcC_out_ga(X1, X3)) → U34_g(X1, X2, pcA_in_g(cons(X3, X2)))
U34_g(X1, X2, pcA_out_g(cons(X3, X2))) → pcA_out_g(cons(s(s(0)), cons(X1, X2)))
U27_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U28_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U28_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U29_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U29_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U30_g(X1, X2, X3, multcB_in_gga(s(s(X1)), X2, X5))
U30_g(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U31_g(X1, X2, X3, pcA_in_g(cons(X5, X3)))
U31_g(X1, X2, X3, pcA_out_g(cons(X5, X3))) → pcA_out_g(cons(s(s(s(s(X1)))), cons(X2, X3)))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → U6_G(X1, X2, X3, pA_in_g(cons(X1, cons(X2, X3))))
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → PA_IN_G(cons(X1, cons(X2, X3)))
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → U7_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
U7_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U8_G(X1, X2, X3, multB_in_gga(X1, X2, X4))
U7_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → MULTB_IN_GGA(X1, X2, X4)
MULTB_IN_GGA(X1, s(X2), X3) → U1_GGA(X1, X2, X3, multB_in_gga(X1, X2, X4))
MULTB_IN_GGA(X1, s(X2), X3) → MULTB_IN_GGA(X1, X2, X4)
MULTB_IN_GGA(X1, s(X2), X3) → U2_GGA(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U2_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U3_GGA(X1, X2, X3, sumD_in_gga(X4, X1, X3))
U2_GGA(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → SUMD_IN_GGA(X4, X1, X3)
SUMD_IN_GGA(X1, s(X2), s(X3)) → U4_GGA(X1, X2, X3, sumD_in_gga(X1, X2, X3))
SUMD_IN_GGA(X1, s(X2), s(X3)) → SUMD_IN_GGA(X1, X2, X3)
U7_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U9_G(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U10_G(X1, X2, X3, pA_in_g(cons(X4, X3)))
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → U15_G(X1, X2, pA_in_g(cons(X1, X2)))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → PA_IN_G(cons(X1, X2))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → U16_G(X1, X2, pcA_in_g(cons(X1, X2)))
U16_G(X1, X2, pcA_out_g(cons(X1, X2))) → U17_G(X1, X2, multC_in_ga(X1, X3))
U16_G(X1, X2, pcA_out_g(cons(X1, X2))) → MULTC_IN_GA(X1, X3)
MULTC_IN_GA(s(X1), X2) → U5_GA(X1, X2, multC_in_ga(X1, X3))
MULTC_IN_GA(s(X1), X2) → MULTC_IN_GA(X1, X3)
U16_G(X1, X2, pcA_out_g(cons(X1, X2))) → U18_G(X1, X2, multcC_in_ga(X1, X3))
U18_G(X1, X2, multcC_out_ga(X1, X3)) → U19_G(X1, X2, pA_in_g(cons(X3, X2)))
U18_G(X1, X2, multcC_out_ga(X1, X3)) → PA_IN_G(cons(X3, X2))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U20_G(X1, X2, X3, pA_in_g(cons(X1, cons(X2, X3))))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → PA_IN_G(cons(X1, cons(X2, X3)))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U21_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
U21_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U22_G(X1, X2, X3, multB_in_gga(X1, X2, X4))
U21_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → MULTB_IN_GGA(X1, X2, X4)
U21_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U23_G(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U23_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U24_G(X1, X2, X3, pA_in_g(cons(X4, X3)))
U23_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
PA_IN_G(cons(0, cons(0, X1))) → U25_G(X1, pA_in_g(X1))
PA_IN_G(cons(0, cons(0, X1))) → PA_IN_G(X1)
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U11_G(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U11_G(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U12_G(X1, X2, X3, multB_in_gga(s(s(X1)), X2, X5))
U11_G(X1, X2, X3, pcA_out_g(cons(X4, X3))) → MULTB_IN_GGA(s(s(X1)), X2, X5)
U11_G(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U13_G(X1, X2, X3, multcB_in_gga(s(s(X1)), X2, X5))
U13_G(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U14_G(X1, X2, X3, pA_in_g(cons(X5, X3)))
U13_G(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → PA_IN_G(cons(X5, X3))
pcA_in_g(cons(X1, nil)) → pcA_out_g(cons(X1, nil))
pcA_in_g(cons(s(s(s(s(X1)))), cons(X2, X3))) → U27_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(s(s(0)), cons(X1, X2))) → U32_g(X1, X2, pcA_in_g(cons(X1, X2)))
pcA_in_g(cons(0, cons(X1, nil))) → pcA_out_g(cons(0, cons(X1, nil)))
pcA_in_g(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U35_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(0, cons(0, X1))) → U38_g(X1, pcA_in_g(X1))
U38_g(X1, pcA_out_g(X1)) → pcA_out_g(cons(0, cons(0, X1)))
U35_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U36_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U39_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U39_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U40_gga(X1, X2, X3, sumcD_in_gga(X4, X1, X3))
sumcD_in_gga(X1, 0, X1) → sumcD_out_gga(X1, 0, X1)
sumcD_in_gga(X1, s(X2), s(X3)) → U41_gga(X1, X2, X3, sumcD_in_gga(X1, X2, X3))
U41_gga(X1, X2, X3, sumcD_out_gga(X1, X2, X3)) → sumcD_out_gga(X1, s(X2), s(X3))
U40_gga(X1, X2, X3, sumcD_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)
U36_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U37_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U37_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → pcA_out_g(cons(0, cons(s(s(X1)), cons(X2, X3))))
U32_g(X1, X2, pcA_out_g(cons(X1, X2))) → U33_g(X1, X2, multcC_in_ga(X1, X3))
multcC_in_ga(0, 0) → multcC_out_ga(0, 0)
multcC_in_ga(s(X1), X2) → U42_ga(X1, X2, multcC_in_ga(X1, X2))
U42_ga(X1, X2, multcC_out_ga(X1, X2)) → multcC_out_ga(s(X1), X2)
U33_g(X1, X2, multcC_out_ga(X1, X3)) → U34_g(X1, X2, pcA_in_g(cons(X3, X2)))
U34_g(X1, X2, pcA_out_g(cons(X3, X2))) → pcA_out_g(cons(s(s(0)), cons(X1, X2)))
U27_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U28_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U28_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U29_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U29_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U30_g(X1, X2, X3, multcB_in_gga(s(s(X1)), X2, X5))
U30_g(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U31_g(X1, X2, X3, pcA_in_g(cons(X5, X3)))
U31_g(X1, X2, X3, pcA_out_g(cons(X5, X3))) → pcA_out_g(cons(s(s(s(s(X1)))), cons(X2, X3)))
MULTC_IN_GA(s(X1), X2) → MULTC_IN_GA(X1, X3)
pcA_in_g(cons(X1, nil)) → pcA_out_g(cons(X1, nil))
pcA_in_g(cons(s(s(s(s(X1)))), cons(X2, X3))) → U27_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(s(s(0)), cons(X1, X2))) → U32_g(X1, X2, pcA_in_g(cons(X1, X2)))
pcA_in_g(cons(0, cons(X1, nil))) → pcA_out_g(cons(0, cons(X1, nil)))
pcA_in_g(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U35_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(0, cons(0, X1))) → U38_g(X1, pcA_in_g(X1))
U38_g(X1, pcA_out_g(X1)) → pcA_out_g(cons(0, cons(0, X1)))
U35_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U36_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U39_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U39_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U40_gga(X1, X2, X3, sumcD_in_gga(X4, X1, X3))
sumcD_in_gga(X1, 0, X1) → sumcD_out_gga(X1, 0, X1)
sumcD_in_gga(X1, s(X2), s(X3)) → U41_gga(X1, X2, X3, sumcD_in_gga(X1, X2, X3))
U41_gga(X1, X2, X3, sumcD_out_gga(X1, X2, X3)) → sumcD_out_gga(X1, s(X2), s(X3))
U40_gga(X1, X2, X3, sumcD_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)
U36_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U37_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U37_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → pcA_out_g(cons(0, cons(s(s(X1)), cons(X2, X3))))
U32_g(X1, X2, pcA_out_g(cons(X1, X2))) → U33_g(X1, X2, multcC_in_ga(X1, X3))
multcC_in_ga(0, 0) → multcC_out_ga(0, 0)
multcC_in_ga(s(X1), X2) → U42_ga(X1, X2, multcC_in_ga(X1, X2))
U42_ga(X1, X2, multcC_out_ga(X1, X2)) → multcC_out_ga(s(X1), X2)
U33_g(X1, X2, multcC_out_ga(X1, X3)) → U34_g(X1, X2, pcA_in_g(cons(X3, X2)))
U34_g(X1, X2, pcA_out_g(cons(X3, X2))) → pcA_out_g(cons(s(s(0)), cons(X1, X2)))
U27_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U28_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U28_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U29_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U29_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U30_g(X1, X2, X3, multcB_in_gga(s(s(X1)), X2, X5))
U30_g(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U31_g(X1, X2, X3, pcA_in_g(cons(X5, X3)))
U31_g(X1, X2, X3, pcA_out_g(cons(X5, X3))) → pcA_out_g(cons(s(s(s(s(X1)))), cons(X2, X3)))
MULTC_IN_GA(s(X1), X2) → MULTC_IN_GA(X1, X3)
MULTC_IN_GA(s(X1)) → MULTC_IN_GA(X1)
From the DPs we obtained the following set of size-change graphs:
SUMD_IN_GGA(X1, s(X2), s(X3)) → SUMD_IN_GGA(X1, X2, X3)
pcA_in_g(cons(X1, nil)) → pcA_out_g(cons(X1, nil))
pcA_in_g(cons(s(s(s(s(X1)))), cons(X2, X3))) → U27_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(s(s(0)), cons(X1, X2))) → U32_g(X1, X2, pcA_in_g(cons(X1, X2)))
pcA_in_g(cons(0, cons(X1, nil))) → pcA_out_g(cons(0, cons(X1, nil)))
pcA_in_g(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U35_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(0, cons(0, X1))) → U38_g(X1, pcA_in_g(X1))
U38_g(X1, pcA_out_g(X1)) → pcA_out_g(cons(0, cons(0, X1)))
U35_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U36_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U39_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U39_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U40_gga(X1, X2, X3, sumcD_in_gga(X4, X1, X3))
sumcD_in_gga(X1, 0, X1) → sumcD_out_gga(X1, 0, X1)
sumcD_in_gga(X1, s(X2), s(X3)) → U41_gga(X1, X2, X3, sumcD_in_gga(X1, X2, X3))
U41_gga(X1, X2, X3, sumcD_out_gga(X1, X2, X3)) → sumcD_out_gga(X1, s(X2), s(X3))
U40_gga(X1, X2, X3, sumcD_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)
U36_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U37_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U37_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → pcA_out_g(cons(0, cons(s(s(X1)), cons(X2, X3))))
U32_g(X1, X2, pcA_out_g(cons(X1, X2))) → U33_g(X1, X2, multcC_in_ga(X1, X3))
multcC_in_ga(0, 0) → multcC_out_ga(0, 0)
multcC_in_ga(s(X1), X2) → U42_ga(X1, X2, multcC_in_ga(X1, X2))
U42_ga(X1, X2, multcC_out_ga(X1, X2)) → multcC_out_ga(s(X1), X2)
U33_g(X1, X2, multcC_out_ga(X1, X3)) → U34_g(X1, X2, pcA_in_g(cons(X3, X2)))
U34_g(X1, X2, pcA_out_g(cons(X3, X2))) → pcA_out_g(cons(s(s(0)), cons(X1, X2)))
U27_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U28_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U28_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U29_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U29_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U30_g(X1, X2, X3, multcB_in_gga(s(s(X1)), X2, X5))
U30_g(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U31_g(X1, X2, X3, pcA_in_g(cons(X5, X3)))
U31_g(X1, X2, X3, pcA_out_g(cons(X5, X3))) → pcA_out_g(cons(s(s(s(s(X1)))), cons(X2, X3)))
SUMD_IN_GGA(X1, s(X2), s(X3)) → SUMD_IN_GGA(X1, X2, X3)
SUMD_IN_GGA(X1, s(X2)) → SUMD_IN_GGA(X1, X2)
From the DPs we obtained the following set of size-change graphs:
MULTB_IN_GGA(X1, s(X2), X3) → MULTB_IN_GGA(X1, X2, X4)
pcA_in_g(cons(X1, nil)) → pcA_out_g(cons(X1, nil))
pcA_in_g(cons(s(s(s(s(X1)))), cons(X2, X3))) → U27_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(s(s(0)), cons(X1, X2))) → U32_g(X1, X2, pcA_in_g(cons(X1, X2)))
pcA_in_g(cons(0, cons(X1, nil))) → pcA_out_g(cons(0, cons(X1, nil)))
pcA_in_g(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U35_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(0, cons(0, X1))) → U38_g(X1, pcA_in_g(X1))
U38_g(X1, pcA_out_g(X1)) → pcA_out_g(cons(0, cons(0, X1)))
U35_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U36_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U39_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U39_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U40_gga(X1, X2, X3, sumcD_in_gga(X4, X1, X3))
sumcD_in_gga(X1, 0, X1) → sumcD_out_gga(X1, 0, X1)
sumcD_in_gga(X1, s(X2), s(X3)) → U41_gga(X1, X2, X3, sumcD_in_gga(X1, X2, X3))
U41_gga(X1, X2, X3, sumcD_out_gga(X1, X2, X3)) → sumcD_out_gga(X1, s(X2), s(X3))
U40_gga(X1, X2, X3, sumcD_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)
U36_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U37_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U37_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → pcA_out_g(cons(0, cons(s(s(X1)), cons(X2, X3))))
U32_g(X1, X2, pcA_out_g(cons(X1, X2))) → U33_g(X1, X2, multcC_in_ga(X1, X3))
multcC_in_ga(0, 0) → multcC_out_ga(0, 0)
multcC_in_ga(s(X1), X2) → U42_ga(X1, X2, multcC_in_ga(X1, X2))
U42_ga(X1, X2, multcC_out_ga(X1, X2)) → multcC_out_ga(s(X1), X2)
U33_g(X1, X2, multcC_out_ga(X1, X3)) → U34_g(X1, X2, pcA_in_g(cons(X3, X2)))
U34_g(X1, X2, pcA_out_g(cons(X3, X2))) → pcA_out_g(cons(s(s(0)), cons(X1, X2)))
U27_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U28_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U28_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U29_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U29_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U30_g(X1, X2, X3, multcB_in_gga(s(s(X1)), X2, X5))
U30_g(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U31_g(X1, X2, X3, pcA_in_g(cons(X5, X3)))
U31_g(X1, X2, X3, pcA_out_g(cons(X5, X3))) → pcA_out_g(cons(s(s(s(s(X1)))), cons(X2, X3)))
MULTB_IN_GGA(X1, s(X2), X3) → MULTB_IN_GGA(X1, X2, X4)
MULTB_IN_GGA(X1, s(X2)) → MULTB_IN_GGA(X1, X2)
From the DPs we obtained the following set of size-change graphs:
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → U7_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
U7_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U9_G(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → PA_IN_G(cons(X1, cons(X2, X3)))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → PA_IN_G(cons(X1, X2))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → U16_G(X1, X2, pcA_in_g(cons(X1, X2)))
U16_G(X1, X2, pcA_out_g(cons(X1, X2))) → U18_G(X1, X2, multcC_in_ga(X1, X3))
U18_G(X1, X2, multcC_out_ga(X1, X3)) → PA_IN_G(cons(X3, X2))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → PA_IN_G(cons(X1, cons(X2, X3)))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U21_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
U21_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U23_G(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U23_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
PA_IN_G(cons(0, cons(0, X1))) → PA_IN_G(X1)
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U11_G(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U11_G(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U13_G(X1, X2, X3, multcB_in_gga(s(s(X1)), X2, X5))
U13_G(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → PA_IN_G(cons(X5, X3))
pcA_in_g(cons(X1, nil)) → pcA_out_g(cons(X1, nil))
pcA_in_g(cons(s(s(s(s(X1)))), cons(X2, X3))) → U27_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(s(s(0)), cons(X1, X2))) → U32_g(X1, X2, pcA_in_g(cons(X1, X2)))
pcA_in_g(cons(0, cons(X1, nil))) → pcA_out_g(cons(0, cons(X1, nil)))
pcA_in_g(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U35_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(0, cons(0, X1))) → U38_g(X1, pcA_in_g(X1))
U38_g(X1, pcA_out_g(X1)) → pcA_out_g(cons(0, cons(0, X1)))
U35_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U36_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
multcB_in_gga(X1, 0, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2), X3) → U39_gga(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U39_gga(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U40_gga(X1, X2, X3, sumcD_in_gga(X4, X1, X3))
sumcD_in_gga(X1, 0, X1) → sumcD_out_gga(X1, 0, X1)
sumcD_in_gga(X1, s(X2), s(X3)) → U41_gga(X1, X2, X3, sumcD_in_gga(X1, X2, X3))
U41_gga(X1, X2, X3, sumcD_out_gga(X1, X2, X3)) → sumcD_out_gga(X1, s(X2), s(X3))
U40_gga(X1, X2, X3, sumcD_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)
U36_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U37_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U37_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → pcA_out_g(cons(0, cons(s(s(X1)), cons(X2, X3))))
U32_g(X1, X2, pcA_out_g(cons(X1, X2))) → U33_g(X1, X2, multcC_in_ga(X1, X3))
multcC_in_ga(0, 0) → multcC_out_ga(0, 0)
multcC_in_ga(s(X1), X2) → U42_ga(X1, X2, multcC_in_ga(X1, X2))
U42_ga(X1, X2, multcC_out_ga(X1, X2)) → multcC_out_ga(s(X1), X2)
U33_g(X1, X2, multcC_out_ga(X1, X3)) → U34_g(X1, X2, pcA_in_g(cons(X3, X2)))
U34_g(X1, X2, pcA_out_g(cons(X3, X2))) → pcA_out_g(cons(s(s(0)), cons(X1, X2)))
U27_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U28_g(X1, X2, X3, multcB_in_gga(X1, X2, X4))
U28_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U29_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U29_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U30_g(X1, X2, X3, multcB_in_gga(s(s(X1)), X2, X5))
U30_g(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U31_g(X1, X2, X3, pcA_in_g(cons(X5, X3)))
U31_g(X1, X2, X3, pcA_out_g(cons(X5, X3))) → pcA_out_g(cons(s(s(s(s(X1)))), cons(X2, X3)))
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → U7_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
U7_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U9_G(X1, X2, X3, multcB_in_gga(X1, X2))
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → PA_IN_G(cons(X1, cons(X2, X3)))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → PA_IN_G(cons(X1, X2))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → U16_G(X1, X2, pcA_in_g(cons(X1, X2)))
U16_G(X1, X2, pcA_out_g(cons(X1, X2))) → U18_G(X1, X2, multcC_in_ga(X1))
U18_G(X1, X2, multcC_out_ga(X1, X3)) → PA_IN_G(cons(X3, X2))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → PA_IN_G(cons(X1, cons(X2, X3)))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U21_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
U21_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U23_G(X1, X2, X3, multcB_in_gga(X1, X2))
U23_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
PA_IN_G(cons(0, cons(0, X1))) → PA_IN_G(X1)
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U11_G(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U11_G(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U13_G(X1, X2, X3, multcB_in_gga(s(s(X1)), X2))
U13_G(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → PA_IN_G(cons(X5, X3))
pcA_in_g(cons(X1, nil)) → pcA_out_g(cons(X1, nil))
pcA_in_g(cons(s(s(s(s(X1)))), cons(X2, X3))) → U27_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(s(s(0)), cons(X1, X2))) → U32_g(X1, X2, pcA_in_g(cons(X1, X2)))
pcA_in_g(cons(0, cons(X1, nil))) → pcA_out_g(cons(0, cons(X1, nil)))
pcA_in_g(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U35_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(0, cons(0, X1))) → U38_g(X1, pcA_in_g(X1))
U38_g(X1, pcA_out_g(X1)) → pcA_out_g(cons(0, cons(0, X1)))
U35_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U36_g(X1, X2, X3, multcB_in_gga(X1, X2))
multcB_in_gga(X1, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2)) → U39_gga(X1, X2, multcB_in_gga(X1, X2))
U39_gga(X1, X2, multcB_out_gga(X1, X2, X4)) → U40_gga(X1, X2, sumcD_in_gga(X4, X1))
sumcD_in_gga(X1, 0) → sumcD_out_gga(X1, 0, X1)
sumcD_in_gga(X1, s(X2)) → U41_gga(X1, X2, sumcD_in_gga(X1, X2))
U41_gga(X1, X2, sumcD_out_gga(X1, X2, X3)) → sumcD_out_gga(X1, s(X2), s(X3))
U40_gga(X1, X2, sumcD_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)
U36_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U37_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U37_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → pcA_out_g(cons(0, cons(s(s(X1)), cons(X2, X3))))
U32_g(X1, X2, pcA_out_g(cons(X1, X2))) → U33_g(X1, X2, multcC_in_ga(X1))
multcC_in_ga(0) → multcC_out_ga(0, 0)
multcC_in_ga(s(X1)) → U42_ga(X1, multcC_in_ga(X1))
U42_ga(X1, multcC_out_ga(X1, X2)) → multcC_out_ga(s(X1), X2)
U33_g(X1, X2, multcC_out_ga(X1, X3)) → U34_g(X1, X2, pcA_in_g(cons(X3, X2)))
U34_g(X1, X2, pcA_out_g(cons(X3, X2))) → pcA_out_g(cons(s(s(0)), cons(X1, X2)))
U27_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U28_g(X1, X2, X3, multcB_in_gga(X1, X2))
U28_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U29_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U29_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U30_g(X1, X2, X3, multcB_in_gga(s(s(X1)), X2))
U30_g(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U31_g(X1, X2, X3, pcA_in_g(cons(X5, X3)))
U31_g(X1, X2, X3, pcA_out_g(cons(X5, X3))) → pcA_out_g(cons(s(s(s(s(X1)))), cons(X2, X3)))
pcA_in_g(x0)
U38_g(x0, x1)
U35_g(x0, x1, x2, x3)
multcB_in_gga(x0, x1)
U39_gga(x0, x1, x2)
sumcD_in_gga(x0, x1)
U41_gga(x0, x1, x2)
U40_gga(x0, x1, x2)
U36_g(x0, x1, x2, x3)
U37_g(x0, x1, x2, x3)
U32_g(x0, x1, x2)
multcC_in_ga(x0)
U42_ga(x0, x1)
U33_g(x0, x1, x2)
U34_g(x0, x1, x2)
U27_g(x0, x1, x2, x3)
U28_g(x0, x1, x2, x3)
U29_g(x0, x1, x2, x3)
U30_g(x0, x1, x2, x3)
U31_g(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → U7_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → PA_IN_G(cons(X1, X2))
PA_IN_G(cons(s(s(0)), cons(X1, X2))) → U16_G(X1, X2, pcA_in_g(cons(X1, X2)))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → PA_IN_G(cons(X1, cons(X2, X3)))
PA_IN_G(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U21_G(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
PA_IN_G(cons(0, cons(0, X1))) → PA_IN_G(X1)
POL(0) = 0
POL(PA_IN_G(x1)) = x1
POL(U11_G(x1, x2, x3, x4)) = 1 + x3
POL(U13_G(x1, x2, x3, x4)) = 1 + x3
POL(U16_G(x1, x2, x3)) = 1 + x2
POL(U18_G(x1, x2, x3)) = 1 + x2
POL(U21_G(x1, x2, x3, x4)) = 1 + x3
POL(U23_G(x1, x2, x3, x4)) = 1 + x3
POL(U27_g(x1, x2, x3, x4)) = 0
POL(U28_g(x1, x2, x3, x4)) = 0
POL(U29_g(x1, x2, x3, x4)) = 0
POL(U30_g(x1, x2, x3, x4)) = 0
POL(U31_g(x1, x2, x3, x4)) = 0
POL(U32_g(x1, x2, x3)) = 0
POL(U33_g(x1, x2, x3)) = 0
POL(U34_g(x1, x2, x3)) = 0
POL(U35_g(x1, x2, x3, x4)) = 0
POL(U36_g(x1, x2, x3, x4)) = 0
POL(U37_g(x1, x2, x3, x4)) = 0
POL(U38_g(x1, x2)) = 0
POL(U39_gga(x1, x2, x3)) = 0
POL(U40_gga(x1, x2, x3)) = 0
POL(U41_gga(x1, x2, x3)) = 0
POL(U42_ga(x1, x2)) = 0
POL(U7_G(x1, x2, x3, x4)) = 1 + x3
POL(U9_G(x1, x2, x3, x4)) = 1 + x3
POL(cons(x1, x2)) = 1 + x2
POL(multcB_in_gga(x1, x2)) = 0
POL(multcB_out_gga(x1, x2, x3)) = 0
POL(multcC_in_ga(x1)) = 0
POL(multcC_out_ga(x1, x2)) = 0
POL(nil) = 0
POL(pcA_in_g(x1)) = 0
POL(pcA_out_g(x1)) = 0
POL(s(x1)) = 0
POL(sumcD_in_gga(x1, x2)) = 0
POL(sumcD_out_gga(x1, x2, x3)) = 0
U7_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U9_G(X1, X2, X3, multcB_in_gga(X1, X2))
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → PA_IN_G(cons(X1, cons(X2, X3)))
U16_G(X1, X2, pcA_out_g(cons(X1, X2))) → U18_G(X1, X2, multcC_in_ga(X1))
U18_G(X1, X2, multcC_out_ga(X1, X3)) → PA_IN_G(cons(X3, X2))
U21_G(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U23_G(X1, X2, X3, multcB_in_gga(X1, X2))
U23_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → PA_IN_G(cons(X4, X3))
U9_G(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U11_G(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U11_G(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U13_G(X1, X2, X3, multcB_in_gga(s(s(X1)), X2))
U13_G(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → PA_IN_G(cons(X5, X3))
pcA_in_g(cons(X1, nil)) → pcA_out_g(cons(X1, nil))
pcA_in_g(cons(s(s(s(s(X1)))), cons(X2, X3))) → U27_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(s(s(0)), cons(X1, X2))) → U32_g(X1, X2, pcA_in_g(cons(X1, X2)))
pcA_in_g(cons(0, cons(X1, nil))) → pcA_out_g(cons(0, cons(X1, nil)))
pcA_in_g(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U35_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(0, cons(0, X1))) → U38_g(X1, pcA_in_g(X1))
U38_g(X1, pcA_out_g(X1)) → pcA_out_g(cons(0, cons(0, X1)))
U35_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U36_g(X1, X2, X3, multcB_in_gga(X1, X2))
multcB_in_gga(X1, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2)) → U39_gga(X1, X2, multcB_in_gga(X1, X2))
U39_gga(X1, X2, multcB_out_gga(X1, X2, X4)) → U40_gga(X1, X2, sumcD_in_gga(X4, X1))
sumcD_in_gga(X1, 0) → sumcD_out_gga(X1, 0, X1)
sumcD_in_gga(X1, s(X2)) → U41_gga(X1, X2, sumcD_in_gga(X1, X2))
U41_gga(X1, X2, sumcD_out_gga(X1, X2, X3)) → sumcD_out_gga(X1, s(X2), s(X3))
U40_gga(X1, X2, sumcD_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)
U36_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U37_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U37_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → pcA_out_g(cons(0, cons(s(s(X1)), cons(X2, X3))))
U32_g(X1, X2, pcA_out_g(cons(X1, X2))) → U33_g(X1, X2, multcC_in_ga(X1))
multcC_in_ga(0) → multcC_out_ga(0, 0)
multcC_in_ga(s(X1)) → U42_ga(X1, multcC_in_ga(X1))
U42_ga(X1, multcC_out_ga(X1, X2)) → multcC_out_ga(s(X1), X2)
U33_g(X1, X2, multcC_out_ga(X1, X3)) → U34_g(X1, X2, pcA_in_g(cons(X3, X2)))
U34_g(X1, X2, pcA_out_g(cons(X3, X2))) → pcA_out_g(cons(s(s(0)), cons(X1, X2)))
U27_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U28_g(X1, X2, X3, multcB_in_gga(X1, X2))
U28_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U29_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U29_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U30_g(X1, X2, X3, multcB_in_gga(s(s(X1)), X2))
U30_g(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U31_g(X1, X2, X3, pcA_in_g(cons(X5, X3)))
U31_g(X1, X2, X3, pcA_out_g(cons(X5, X3))) → pcA_out_g(cons(s(s(s(s(X1)))), cons(X2, X3)))
pcA_in_g(x0)
U38_g(x0, x1)
U35_g(x0, x1, x2, x3)
multcB_in_gga(x0, x1)
U39_gga(x0, x1, x2)
sumcD_in_gga(x0, x1)
U41_gga(x0, x1, x2)
U40_gga(x0, x1, x2)
U36_g(x0, x1, x2, x3)
U37_g(x0, x1, x2, x3)
U32_g(x0, x1, x2)
multcC_in_ga(x0)
U42_ga(x0, x1)
U33_g(x0, x1, x2)
U34_g(x0, x1, x2)
U27_g(x0, x1, x2, x3)
U28_g(x0, x1, x2, x3)
U29_g(x0, x1, x2, x3)
U30_g(x0, x1, x2, x3)
U31_g(x0, x1, x2, x3)
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → PA_IN_G(cons(X1, cons(X2, X3)))
pcA_in_g(cons(X1, nil)) → pcA_out_g(cons(X1, nil))
pcA_in_g(cons(s(s(s(s(X1)))), cons(X2, X3))) → U27_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(s(s(0)), cons(X1, X2))) → U32_g(X1, X2, pcA_in_g(cons(X1, X2)))
pcA_in_g(cons(0, cons(X1, nil))) → pcA_out_g(cons(0, cons(X1, nil)))
pcA_in_g(cons(0, cons(s(s(X1)), cons(X2, X3)))) → U35_g(X1, X2, X3, pcA_in_g(cons(X1, cons(X2, X3))))
pcA_in_g(cons(0, cons(0, X1))) → U38_g(X1, pcA_in_g(X1))
U38_g(X1, pcA_out_g(X1)) → pcA_out_g(cons(0, cons(0, X1)))
U35_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U36_g(X1, X2, X3, multcB_in_gga(X1, X2))
multcB_in_gga(X1, 0) → multcB_out_gga(X1, 0, 0)
multcB_in_gga(X1, s(X2)) → U39_gga(X1, X2, multcB_in_gga(X1, X2))
U39_gga(X1, X2, multcB_out_gga(X1, X2, X4)) → U40_gga(X1, X2, sumcD_in_gga(X4, X1))
sumcD_in_gga(X1, 0) → sumcD_out_gga(X1, 0, X1)
sumcD_in_gga(X1, s(X2)) → U41_gga(X1, X2, sumcD_in_gga(X1, X2))
U41_gga(X1, X2, sumcD_out_gga(X1, X2, X3)) → sumcD_out_gga(X1, s(X2), s(X3))
U40_gga(X1, X2, sumcD_out_gga(X4, X1, X3)) → multcB_out_gga(X1, s(X2), X3)
U36_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U37_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U37_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → pcA_out_g(cons(0, cons(s(s(X1)), cons(X2, X3))))
U32_g(X1, X2, pcA_out_g(cons(X1, X2))) → U33_g(X1, X2, multcC_in_ga(X1))
multcC_in_ga(0) → multcC_out_ga(0, 0)
multcC_in_ga(s(X1)) → U42_ga(X1, multcC_in_ga(X1))
U42_ga(X1, multcC_out_ga(X1, X2)) → multcC_out_ga(s(X1), X2)
U33_g(X1, X2, multcC_out_ga(X1, X3)) → U34_g(X1, X2, pcA_in_g(cons(X3, X2)))
U34_g(X1, X2, pcA_out_g(cons(X3, X2))) → pcA_out_g(cons(s(s(0)), cons(X1, X2)))
U27_g(X1, X2, X3, pcA_out_g(cons(X1, cons(X2, X3)))) → U28_g(X1, X2, X3, multcB_in_gga(X1, X2))
U28_g(X1, X2, X3, multcB_out_gga(X1, X2, X4)) → U29_g(X1, X2, X3, pcA_in_g(cons(X4, X3)))
U29_g(X1, X2, X3, pcA_out_g(cons(X4, X3))) → U30_g(X1, X2, X3, multcB_in_gga(s(s(X1)), X2))
U30_g(X1, X2, X3, multcB_out_gga(s(s(X1)), X2, X5)) → U31_g(X1, X2, X3, pcA_in_g(cons(X5, X3)))
U31_g(X1, X2, X3, pcA_out_g(cons(X5, X3))) → pcA_out_g(cons(s(s(s(s(X1)))), cons(X2, X3)))
pcA_in_g(x0)
U38_g(x0, x1)
U35_g(x0, x1, x2, x3)
multcB_in_gga(x0, x1)
U39_gga(x0, x1, x2)
sumcD_in_gga(x0, x1)
U41_gga(x0, x1, x2)
U40_gga(x0, x1, x2)
U36_g(x0, x1, x2, x3)
U37_g(x0, x1, x2, x3)
U32_g(x0, x1, x2)
multcC_in_ga(x0)
U42_ga(x0, x1)
U33_g(x0, x1, x2)
U34_g(x0, x1, x2)
U27_g(x0, x1, x2, x3)
U28_g(x0, x1, x2, x3)
U29_g(x0, x1, x2, x3)
U30_g(x0, x1, x2, x3)
U31_g(x0, x1, x2, x3)
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → PA_IN_G(cons(X1, cons(X2, X3)))
pcA_in_g(x0)
U38_g(x0, x1)
U35_g(x0, x1, x2, x3)
multcB_in_gga(x0, x1)
U39_gga(x0, x1, x2)
sumcD_in_gga(x0, x1)
U41_gga(x0, x1, x2)
U40_gga(x0, x1, x2)
U36_g(x0, x1, x2, x3)
U37_g(x0, x1, x2, x3)
U32_g(x0, x1, x2)
multcC_in_ga(x0)
U42_ga(x0, x1)
U33_g(x0, x1, x2)
U34_g(x0, x1, x2)
U27_g(x0, x1, x2, x3)
U28_g(x0, x1, x2, x3)
U29_g(x0, x1, x2, x3)
U30_g(x0, x1, x2, x3)
U31_g(x0, x1, x2, x3)
pcA_in_g(x0)
U38_g(x0, x1)
U35_g(x0, x1, x2, x3)
multcB_in_gga(x0, x1)
U39_gga(x0, x1, x2)
sumcD_in_gga(x0, x1)
U41_gga(x0, x1, x2)
U40_gga(x0, x1, x2)
U36_g(x0, x1, x2, x3)
U37_g(x0, x1, x2, x3)
U32_g(x0, x1, x2)
multcC_in_ga(x0)
U42_ga(x0, x1)
U33_g(x0, x1, x2)
U34_g(x0, x1, x2)
U27_g(x0, x1, x2, x3)
U28_g(x0, x1, x2, x3)
U29_g(x0, x1, x2, x3)
U30_g(x0, x1, x2, x3)
U31_g(x0, x1, x2, x3)
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → PA_IN_G(cons(X1, cons(X2, X3)))
No rules are removed from R.
PA_IN_G(cons(s(s(s(s(X1)))), cons(X2, X3))) → PA_IN_G(cons(X1, cons(X2, X3)))
POL(PA_IN_G(x1)) = x1
POL(cons(x1, x2)) = x1 + x2
POL(s(x1)) = x1